COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	Which scheme more adequately reflects our intuitions about properties of function?
C00004 ENDMK
C⊗;
Which scheme more adequately reflects our intuitions about properties of function?
The dynamic binding scheme implements the notion of  procedure 
application %3f[t]%1 being the
substitution of a copy  of the body %3f%1 with every occurrence of a formal
parameter replaced with %3t%1.

.GROUP;
We shall restrict out discussion to unary λ-expressions. With that
restriction, the dynamic substitution
 can be expressed as:

.BEGIN SELECT 3;TABIT3(17,26,35);GROUP;

subst <= λ[[x;y;z]\[is_var[z] → [equal[y;z] → x; %et%3 → z];
\ is_app[z] → mk_app[\subst[x;y;func[z]]
\\\subst[x;y;arglist[z]]];
\ eq[y;λ_var[z]] → z;
\ %et%3 → mk_λ[\λ_var[z];
\\subst[x;y;body[z]]]]]
.END
.APART;

However, some implications of dynamic binding are in conflict with 
other properties we expect functions to possess. For example, we expect

******
LISP does not use explicit substitution, but rather simulates the substitution
 using symbol tables.
LISP embodies %3subst%1   with the exception that
the %3function%1#construct simulates %3subst%9'%1. As we have seen,
the use of %3subst%1 can lead to unexpected results. The formal study
of functionality  which appears in the %9λ%1-calculus is based on %3subst%9'%1.